from cheqed.core.graph.node import Node
from cheqed.core.proof import Rule
from cheqed.core import proof, theory, qparse
from cheqed.core.rules import primitive
from cheqed.core.sequent import Sequent

from cheqed.core.rules.match import match_first
from cheqed.core import side

def applicable(side, pattern):
    def is_applicable(sequent):
        try:
            match_first(sequent, side, pattern)
            return True
        except:
            return False
        
    def decorator(fun):
        fun.is_applicable = is_applicable
        return fun

    return decorator

def noop():
    return Node(Rule(None, 'noop()'), 1, 0)

def sequence(*seq):
    if len(seq) == 0:
        return noop()
    seq = list(seq)
    first = seq.pop(0)
    current = first
    while seq:
        next = seq.pop(0)
        goals = proof.goals(current)
        if len(goals) != 1:
            raise 'sequence: all items must have a single goal.'
        if len(next.bottom) != 1:
            raise 'sequence: all items must have a single bottom.'
        if next.rule.serialize() != 'noop()':
            goals[0].connect(next.bottom[0])
            current = next
    return first

def split(node, *branches):
    goals = proof.goals(node)
    if len(goals) != len(branches):
        raise 'split: number of goals must equal number of branches.'
    for goal, branch in zip(goals, branches):
        if len(branch.bottom) != 1:
            raise 'split: all branches must have a single bottom.'
        if branch.rule.serialize() != 'noop()':
            goal.connect(branch.bottom[0])
    return node

parser = theory.parser
printer = qparse.TermPrinter(parser)

def parse(term):
    return parser.parse(term)

def prettyprint(term):
    return printer.term(term)

# def make_rule(primitive):
#     args, varargs, varkw, defaults = inspect.getargspec(primitive)
#     assert args[0] == 'sequent'
#     ser_args = []
#     for arg in args:
#         if arg == 'index':

__all__ = [
    'axiom', 'cut',
    'left_permutation', 'right_permutation',
    'left_weakening', 'right_weakening',
    'left_negation', 'right_negation',
    'left_substitution', 'right_substitution',
    'left_symmetry', 'right_symmetry',
    'left_disjunction', 'right_disjunction',
    'left_conjunction', 'right_conjunction',
    'left_implication', 'right_implication',
    'left_bidirectional', 'right_bidirectional',
    'left_universal', 'right_universal',
    'left_schema',
    'left_existential', 'right_existential',
    'right_separation',
    'left_subset', 'right_subset',
    'left_extensionality', 'right_extensionality',
    'right_extension',
    ]

def left_weakening():
    return Node(Rule(primitive.left_weakening, 'left_weakening()'), 1, 1)

def right_weakening():
    return Node(Rule(primitive.right_weakening, 'right_weakening()'), 1, 1)

def left_permutation(index):
    return Node(Rule(lambda x: primitive.left_permutation(x, index),
                     'left_permutation(%d)' % index),
                1, 1)

def right_permutation(index):
    return Node(Rule(lambda x: primitive.right_permutation(x, index),
                     'right_permutation(%d)' % index),
                1, 1)

def axiom():
    return Node(Rule(primitive.axiom, 'axiom()'), 1, 0)

def left_substitution():
    return Node(Rule(primitive.left_substitution, 'left_substitution()'), 1, 1)

def right_substitution():
    return Node(Rule(primitive.right_substitution, 'right_substitution()'), 1, 1)

def left_symmetry():
    return Node(Rule(primitive.left_symmetry, 'left_symmetry()'), 1, 1)

def right_symmetry():
    return Node(Rule(primitive.right_symmetry, 'right_symmetry()'), 1, 1)

def left_negation():
    return Node(Rule(primitive.left_negation, 'left_negation()'), 1, 1)

def right_negation():
    return Node(Rule(primitive.right_negation, 'right_negation()'), 1, 1)

def left_disjunction():
    return Node(Rule(primitive.left_disjunction, 'left_disjunction()'), 1, 2)

def right_disjunction():
    return Node(Rule(primitive.right_disjunction, 'right_disjunction()'), 1, 1)

@applicable(side.LEFT, 'for_all x . phi')
def left_universal(witness):
    return Node(Rule(lambda x: primitive.left_universal(x, witness),
                     "left_universal(parse(r'%s'))"
                     % prettyprint(witness)),
                1, 1)

@applicable(side.RIGHT, 'for_all x . phi')
def right_universal(witness):
    return Node(Rule(lambda x: primitive.right_universal(x, witness),
                     "right_universal(parse(r'%s'))"
                     % prettyprint(witness)),
                1, 1)

@applicable(side.LEFT, 'schema phi . psi')
def left_schema(witness):
    return Node(Rule(lambda x: primitive.left_schema(x, witness),
                     "left_schema(parse(r'%s'))"
                     % prettyprint(witness)),
                1, 1)

def right_separation():
    return Node(Rule(primitive.right_separation, 'right_separation()'), 1, 1)

def goal(term):
    def _goal():
        return [Sequent([], [term])]
    return Node(Rule(_goal, "goal(parse(r'%s'))" % prettyprint(term)),
                0, 1)

def right_conjunction():
    return sequence(cut('and.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_negation(),
                    split(left_disjunction(),
                          left_negation(),
                          left_negation()))

def left_conjunction():
    return sequence(cut('and.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_negation(),
                    right_disjunction(),
                    right_negation(),
                    right_negation(),
                    left_permutation(1))

def left_implication():
    return sequence(cut('implies.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    split(left_disjunction(),
                          left_negation(),
                          noop()))

def right_implication():
    return sequence(cut('implies.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_disjunction(),
                    right_negation())

def right_bidirectional():
    return sequence(cut('iff.definition'),
                    right_substitution(),
                    left_weakening(),
                    split(right_conjunction(),
                          right_implication(),
                          right_implication()))

def left_bidirectional():
    return sequence(cut('iff.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_conjunction(),
                    split(left_implication(),
                          split(left_implication(),
                                right_permutation(1),
                                axiom()),
                          sequence(left_permutation(1),
                                   split(left_implication(),
                                         axiom(),
                                         noop()))))

@applicable(side.RIGHT, 'exists x . phi')
def right_existential(witness):
    return sequence(cut('exists.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_negation(),
                    left_universal(witness),
                    left_negation(),
                    left_weakening())

@applicable(side.LEFT, 'exists x . phi')
def left_existential(witness):
    return sequence(cut('exists.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_negation(),
                    right_universal(witness),
                    right_negation())

def left_subset():
    return sequence(cut('subset.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(parse(r'foo')),
                    left_permutation(1),
                    left_weakening(),
                    left_implication())

def right_subset():
    return sequence(cut('subset.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_universal(parse(r'foo')),
                    right_implication())

def left_extensionality():
    return sequence(cut('equals.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(parse(r'foo')),
                    left_permutation(1),
                    left_weakening(),
                    left_bidirectional())

def right_extensionality():
    return sequence(cut('equals.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_universal(parse(r'foo')),
                    right_bidirectional())

def right_extension(sequent):
    match = match_first(sequent, side.RIGHT, 'a = b')
    return sequence(cut('extensionality.axiom'),
                    left_universal(match['a']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(match['b']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(parse(r'foo')),
                    left_permutation(1),
                    left_weakening(),
                    split(left_implication(),
                          right_bidirectional(),
                          axiom()))

def evaluate(string):
    try:
        return eval(string)
    except:
        raise Exception(string)

definitions = {}

def define(name, term):
    definitions[name] = Sequent([], [parse(term)])

#parse('class_of x . a')
#parse('(set_of x . (exists y . a))')
#parse('domain = (\f.(class_of x . (exists y . a)))')
    

define('logic.and.definition',
       r'(and) = (\xx.\yy.(not ((not xx) or (not yy))))')

define('logic.implies.definition',
       r'(implies) = (\x.\y.(not x or y))')

define('logic.iff.definition',
       r'(iff) = (\x.\y.((x implies y) and (y implies x)))')

define('logic.exists.definition',
       r'(exists) = (\x.(not (for_all y . (not x(y)))))')

define('zfc.extensionality',
       r'for_all x . (for_all y . (for_all z . (((z in x) iff (z in y)) implies (x = y))))')

define('zfc.union',
       r'for_all F . (exists A . (for_all Y . (for_all x . (((x in Y) and (Y in F)) implies (x in A)))))')

define('zfc.pairing',
       r'for_all x . (for_all y . (exists z . ((x in z) and (y in z))))')

define('zfc.powerset',
       r'for_all x . (exists y . (for_all z . ((z subset x) implies (z in y))))')

define('zfc.separation',
       r'schema phi . (for_all z . (exists y . (for_all x .' \
       '((x in y) iff ((x in z) and phi)))))')

#define('nbg.comprehension',
#       r'schema phi . (exists A . (for_all x . ((x in_class A) iff phi)))')

#define('nbg.limitation',
#       r'for_all C . ((exists x . (x = C)) iff (not (exists f . is_bijection(f, C, V))))')

#define('class.is_bijection',
#        r'is_bijection = (\f.(\d.(\r.(is_injection(f, d, r) and is_surjection(f, d, r)))))')


#define('class.domain',
#       r'domain = (\f.(class_of x . (exists y . a)))')

# define('class.range',
#        r'range = (\f.(class_of y . (exists x . (ordered_pair(x, y) in_class f))))')

# define('class.is_function',
#        r'is_function = (\f.(for_all x . ((x in_class domain(f)) implies (exists_unique y . (ordered_pair(x, y) in_class f)))))')

define('set.emptyset.definition',
       r'for_all x . (not (x in emptyset))')

define('set.subset.definition',
       r'(subset) = (\x.\y.(for_all z . ((z in x) implies (z in y))))')

#define('set.powerset.definition',
#       r'for_all x . for_all y . ((y in powerset(x)) iff (y subset x))')

define('set.powerset.definition',
       r'powerset = (\x.(set_of y . (y subset x)))') 

#define('set.unordered_pair.definition',
#       r'for_all x . for_all y . for_all z . ((z in unordered_pair(x, y)) iff ((z = x) or (z = y)))')

define('set.unordered_pair.definition',
       r'unordered_pair = (\x.(\y.(set_of z . ((z = x) or (z = y)))))')

# define('set.equals.definition',
#        r'(equals) = (\x.(\y.((for_all z . ((z in x) iff (z in y))) and (for_all z . ((x in z) iff (y in z))))))')

#define('set.ordered_pair.definition',
#       r'ordered_pair = (\x.(\y.(unordered_pair(x, unordered_pair(x, y)))))')

#parse(r'(\a.(\y.(unordered_pair(x, unordered_pair(x, y)))))')
#parse(r'(\a.(\y.(f_p(x, f_p(x, y)))))')

define('set.singleton.definition',
       r'singleton = (\x.(set_of y . (y = x)))')

# define('is_ordered_pair.definition',
#        r'is_ordered_pair = (\x.(exists y . exists z . (x = ordered_pair(y, z))))')

# define('ordered_pair_first.definition',
#        r'for_all x . for_all y . ((x = ordered_pair_first(y)) iff (is_ordered_pair(y)))')



def _cut(sequent, definition):
    return [Sequent(definition.right + sequent.left,
                    sequent.right)]

def cut(name):
    return Node(Rule(lambda x: _cut(x, definitions[name]),
                     "cut('%s')" % name),
                1, 1)

import copy
import inspect

def is_applicable(func, args, goal, sequent):
    if hasattr(func, 'is_applicable'):
        return func.is_applicable(sequent)

    if len(args) > 0:
        return True

    try:
        proof.extend(goal, func())
    except Exception, e:
        return False

    goal.disconnect()
    return True

def applicable_rules(prf):
    goals = proof.goals(prf)
    if len(goals) == 0:
        return []
    goal = proof.goals(prf)[0]
    sequent = proof.sequent(goal)

    rules = []
    for name in __all__:
        func = globals()[name]
        args, varargs, varkw, defaults = inspect.getargspec(func)
        if is_applicable(func, args, goal, sequent):
            rules.append((name, args))

    return rules
